$\forall$${\it es}$:ES, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $e$:E.
\\[0ex]@loc($e$) discrete ${\it ds}$
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$first($e$)))
\\[0ex]$\Rightarrow$ (state after pred($e$) = (state when $e$) $\in$ State(${\it ds}$))